\begin{tabbing}
Generic\{$f$:$\mathbb{N}\rightarrow$$T$$\mid$$S$($f$)\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$R$:($\mathbb{N}\rightarrow$($T$ List)$\rightarrow$Prop).\+
\\[0ex]($\forall$$i$:$\mathbb{N}$, $s$:$T$ List. $\exists$${\it s'}$:$T$ List. $s$ $\leq$ ${\it s'}$ \& $R$($i$,${\it s'}$))
\\[0ex]\& ($\forall$$f$:($\mathbb{N}\rightarrow$$T$). ($\forall$$i$:$\mathbb{N}$. $\exists$$s$:$T$ List. $R$($i$,$s$) \& ($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$s$$\parallel$}}$. $s$[$n$] $=$ $f$($n$))) $\Rightarrow$ $S$($f$))
\-
\end{tabbing}